Definitions | t T, #$n, x:A. B(x), A B, n+m, a<b, Void, x:A![](../FONT/dash.png) B(x), P ![](../FONT/eq.png) Q, False, A, , {x:A| B(x) }, , data(T), Atom$n, left+right, Type, x:A B(x), {i..j }, <a,b>, Prop, True, i![](../FONT/le.png) j, b, ![](../FONT/not.png) b, , s = t, P & Q, i j < k, f(a), x.A(x), ![](../FONT/lam.png) x. t(x), 1of(t), i= j, f[x:=v], i< j, T, P ![](../FONT/if_big.png) Q, P ![](../FONT/if_big.png) Q, Unit, encrypt(tab;keyv), secret-table(T), Id |